Nuprl Lemma : Q-Q-glued-to-self
11,40
postcript
pdf
es
:ES,
A
:Type,
Ia
:AbsInterface(
A
),
Q
:(E
E
). Q-R-glued(
es
;
A
; (
e
.
Ia
(
e
));
Ia
;
Q
;
Ia
;
Q
)
latex
Definitions
s
=
t
,
t
T
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
ES
,
Type
,
AbsInterface(
A
)
,
,
E
,
Q-R-glued(
es
;
Ib_valtype
;
f
;
Ia
;
Qa
;
Ib
;
Rb
)
,
strong-subtype(
A
;
B
)
,
P
Q
,
f
'
Ia
,
X
(
e
)
,
f
(
a
)
,
x
.
A
(
x
)
,
e
X
,
b
,
{
x
:
A
|
B
(
x
)}
,
E(
X
)
,
<
a
,
b
>
,
x
:
A
B
(
x
)
,
left
+
right
,
x
:
A
.
B
(
x
)
,
g
glues
Ia
:
Qa
f
Ib
:
Rb
,
,
a
:
A
fp
B
(
a
)
,
Top
Lemmas
es-interface-val
wf2
,
member
wf
,
top
wf
,
subtype
rel
wf
,
es-E-interface
wf
,
assert
wf
,
es-is-interface
wf
,
es-interface-image-trivial
,
Q-Q-glued-self-image
,
Q-R-glued
wf
,
es-E
wf
,
es-interface
wf
,
event
system
wf
origin
es:ES, A:Type, Ia:AbsInterface(A), Q:(E
E
). Q-R-glued(es; A; (
e.Ia(e)); Ia; Q; Ia; Q) es:ES, A:Type, Ia:AbsInterface(A), Q:(EE). Q-R-glued(es; A; (e.Ia(e)); Ia; Q; Ia; Q) 
T
Q
X
b
B(x)
x:A. B(x)